/*
 * saturation.c
 *
 *  Created on: Jul 22, 2012
 *      Author: baris
 */
#include <string.h>
#include <assert.h>

#include "../model/model.h"
#include "../model/memory_utils.h"
#include "../model/print_utils.h"

#include "locals.h"
#include "utils.h"

void init_saturation() {
	int i;

	// Here we copy the content of tbox->subclass_axioms and tbox->eqclass_axioms to the
	// scheduled_axioms. We could instead use already allocated space tbox->subclass_axioms, but
	// for the case that we might need the original axioms in future extensions we make a copy and
	// leave the original axioms. For now we do not need them so we free tbox->subclass_axioms and
	// tbox->eqclass_axioms.
	scheduled_axiom_count = tbox->subclass_axiom_count;
	scheduled_axioms = (SubClassAxiom**) malloc(scheduled_axiom_count * sizeof(SubClassAxiom*));
	assert(scheduled_axioms != NULL);
	memcpy(scheduled_axioms, tbox->subclass_axioms, scheduled_axiom_count * sizeof(SubClassAxiom*));

	for (i = 0; i < tbox->eqclass_axiom_count; i++) {
		enqueue_to_scheduled_axioms(create_subclass_axiom(tbox->eqclass_axioms[i]->lhs,
				tbox->eqclass_axioms[i]->rhs));
		enqueue_to_scheduled_axioms(create_subclass_axiom(tbox->eqclass_axioms[i]->rhs,
				tbox->eqclass_axioms[i]->lhs));
	}

	free_subclass_axioms(tbox);

	processed_axioms = (Pvoid_t) NULL;

}

void saturate_tbox(TBox* tbox) {
	SubClassAxiom* ax;
	int i, j, lhs_is_subsumed_by_conjunct;
	int it_count = 0;


	ax = dequeue_from_scheduled_axioms();

	while (ax != NULL) {
		if (mark_axiom_processed(ax)) {
			it_count++;
			for (i = 0; i < ax->rhs->told_subsumer_count; i++)
				enqueue_to_scheduled_axioms(create_subclass_axiom(ax->lhs, ax->rhs->told_subsumers[i]));

			for (i = 0; i < ax->rhs->conjunct_of_count; i++) {
				lhs_is_subsumed_by_conjunct = 1;
				for (j = 0; j < ax->rhs->conjunct_of[i]->description.conj->size &&
						lhs_is_subsumed_by_conjunct; j++) {
					J1T(lhs_is_subsumed_by_conjunct, ax->lhs->subsumers, 
							(Word_t) ax->rhs->conjunct_of[i]->description.conj->conjuncts[j]);
				}
				if (lhs_is_subsumed_by_conjunct)
					enqueue_to_scheduled_axioms(create_subclass_axiom(ax->lhs, ax->rhs->conjunct_of[i]));
			}

			switch (ax->rhs->type) {
			case CONJUNCTION:
				for (i = 0; i < ax->rhs->description.conj->size; i++)
					enqueue_to_scheduled_axioms(
							create_subclass_axiom(ax->lhs, ax->rhs->description.conj->conjuncts[i]));
				break;
			case EXISTENTIAL_RESTRICTION:
				enqueue_to_scheduled_axioms(
						create_subclass_axiom(ax->rhs->description.exists->filler,
								ax->rhs->description.exists->filler));
				break;
			// default:
			// 	fprintf(stderr, "unknown concept type, aborting\n");
			// 	break;
			}
		}
		// We are done with the ax, free it. But not the concepts lhs and rhs!
		// They are still used in other axioms
		free(ax);
		ax = dequeue_from_scheduled_axioms();
	}
	printf("\niteration_count: %d\n", it_count);
}
